Journals
  Publication Years
  Keywords
Search within results Open Search
Please wait a minute...
For Selected: Toggle Thumbnails
Synthesis of loop bound functions for loop programs
Wang TAN, Yi LI
Journal of Computer Applications    2022, 42 (2): 565-573.   DOI: 10.11772/j.issn.1001-9081.2021020221
Abstract289)   HTML6)    PDF (596KB)(87)       Save

As the mainstream methods of loop program termination analysis,most existing ranking function methods are limited to the solution of linear or polynomial ranking functions. Concerning that the existing ranking function methods cannot prove the termination if there are no corresponding linear or polynomial ranking functions for the loop programs, a new method was proposed to synthesize the loop bound function for the given loop program. The existence of loop bound function of a given loop program implies the termination of this loop function. Firstly, the problem of solving the loop bound functions was transformed into a linear binary classification problem. Once the function’s template was selected, the mapping relationship was established according to the template to construct the training set. After that, the obtained training set was used to obtain the classification hyperplane through Support Vector Machine (SVM) to find the template coefficients, thereby obtaining the candidate loop bound function. Finally, the existing symbol verification tool Redlog was used to verify this candidate loop bound function. Experimental results show that compared with the existing ranking function methods, the proposed method not only can be applied to more loop programs, but also has the obtained loop bound functions more simplified in form than the ranking functions. Specifically, for some loops without linear ranking functions, the corresponding linear loop bound functions can be solved by the proposed method; at the same time, for some loops with only multiphase linear ranking functions, the global linear loop bound functions can be solved by the proposed method.

Table and Figures | Reference | Related Articles | Metrics